GrpSig
== car:Type
==  (eq:(carcar)
==  le:(carcar)
==  op:(carcarcar)
==  (id:car
==  (carcar))) 

latex

---

clarification:

GrpSig{i}
== car:Type{i}
==  (eq:(carcar)
==  le:(carcar)
==  op:(carcarcar)
==  (id:car
==  (carcar))) 

latex

Up	grp sig object directory
Wellformedness Lemmas	grp sig wf
Definitions